TAJS icon indicating copy to clipboard operation
TAJS copied to clipboard

soundiness

Open amoeller opened this issue 8 years ago • 0 comments

Known sources of unsoundness in the modeling of the core language and native library:

  • properties of 'arguments' should be shared with the formal parameters (currently only supported one way)
  • getters/setters do not behave correctly if they have wrong number of arguments
  • RangeError exceptions caused by stack size exceeded are ignored
  • Unevalizer: variables created via 'eval' should have empty attributes, unlike ordinary variables
  • JSArray.sort ignores comparefn if it is a host object
  • ES5 Object.* methods missing some TypeErrors
  • ES5 strict mode only partly modeled
  • some ES5 native functions are modeled unsoundly by mdn-polyfills.js, including 'bind'
  • not all ES3 to ES5 minor "breaking changes" have been modeled
  • dynamic property write operations are assumed not to write to __proto__

These issues will be fixed "by need" if we find that they cause wrong analysis results on realistic programs.

amoeller avatar Oct 28 '16 13:10 amoeller