dhh1128 / intent

the intent formal language
https://intentlang.org
2 stars 1 forks source link

acquire additional semantics as variable is examined; map them to marks #10

Open dhh1128 opened 10 years ago

dhh1128 commented 10 years ago

screenshot16 Notice in this screenshot that coverity has detected that a variable might be null, based on a test that the code did. Once that information was known, semantics in the next line were demonstrably wrong. Intent needs to ship with a set of marks that work this way, such that we can refine semantics as we examine the value of a variable. For example, if we have a line that says "if len(mystring) < 25", then inside that block, we need to add a +range(1,25) mark to mystring. This should then be passed to all called functions, instead of simply passing the range that the string started with.

dhh1128 commented 10 years ago

Note the false positive from the attached coverity screenshot. Coverity didn't pick up that right before we call MUArrayListGet(), we resize the array so that we're guaranteed to have a valid index. A mark indicating that the size of the array was known to be x because we had just resized would have allowed us to understand that we are guaranteed to have a valid value on line 348.

screenshot17