search

levjj / esverify

ECMAScript verification with SMT solvers
https://esverify.org/
MIT License
123 stars 5 forks source link

Support for mutable objects and array #24

Open levjj opened 5 years ago

levjj commented 5 years ago

esverify currently only supports immutable object literals and arrays.

Improved support for mutability probably requires some redesign of the fundamental base of the vcgen, e.g. segmentation logic or frames/regions.

Example:

const a = [1,2,3];
a.push(4);
assert(a.length === 4);