JSConTest - Test Framework

This test suite runs contracts against a this implementation of a single-linked list.

Anchor	Permissions
this	this._head	,	this._head.*.next	,	this._length	,

Statistic

Number of contracts total:: 6
Number of contracts done:: 1
Number of verified contracts:: 0
Number of failed contracts:: 0
Number of contracts where check exists with an error:: 0
Number of well tested contracts:: 1
Number of tests run:: 50

Warnings (filtered)

f_add1: Effect Error, read access not allowed! You try to read the property _head of object {_length: 0,_head: null}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, write access not allowed! You try to write the property _head of object {_length: 0,_head: null}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, write access not allowed! You try to write the property _length of object {_length: 0,_head: {data: -1814528183,next: null,__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_length","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, read access not allowed! You try to read the property _head of object {_length: 1,_head: {data: -1814528183,next: null,__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, read access not allowed! You try to read the property _head of object {_length: 1,_head: {data: -1814528183,next: null,__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, read access not allowed! You try to read the property next of object {data: -1814528183,next: null,__infos__: {data: {reference: -1814528183,p_map: {0: [-omitted value-,-omitted value-]}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"next","effect":{"effect":{"fname":"f_add1","name":"this","type":2},"type":3,"property":"_head"}}]
f_add1: Effect Error, write access not allowed! You try to write the property next of object {data: -1814528183,next: null,__infos__: {data: {reference: -1814528183,p_map: {0: [-omitted value-,-omitted value-]}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"next","effect":{"effect":{"fname":"f_add1","name":"this","type":2},"type":3,"property":"_head"}}]
f_add1: Effect Error, write access not allowed! You try to write the property _length of object {_length: 1,_head: {data: -1814528183,next: {data: 471161082,next: null,__infos__: {data: {reference: -omitted value-,p_map: -omitted value-}}},__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_length","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, read access not allowed! You try to read the property _head of object {_length: 2,_head: {data: -1814528183,next: {data: 471161082,next: null,__infos__: {data: {reference: -omitted value-,p_map: -omitted value-}}},__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]
f_add1: Effect Error, read access not allowed! You try to read the property _head of object {_length: 2,_head: {data: -1814528183,next: {data: 471161082,next: null,__infos__: {data: {reference: -omitted value-,p_map: -omitted value-}}},__infos__: {data: {reference: -1814528183,p_map: {0: -omitted value-}}}}}. 

Permissions you have to respect: {0: ['f_add1@']}

The following was not respected: ['f_add1@']

[{"type":3,"property":"_head","effect":{"fname":"f_add1","name":"this","type":2}}]

Module: f_add1

Contract 'LList.(integer)~>undefined' is fulfilled by value: function add (data) { var node = {data : data, next : null}, current; if ((this._head === null)) { this._head = node; } else { current = this._head; while (current.next) { current = current.next; } current.next = node; }; this._length++ ; } // (with assert check enabled). Tests run: 50

JSConTest - Test Framework - Linked List

Effect Inference

Effects for Function f_add1

Statistic

Warnings (filtered)

Module: f_add1

Module: f_item3