Additional errors and warnings

[Calvin-L]

Cozy currently issues errors for a number of things: typechecking failures, misuses of the, invariant preservation failures, and so on. There are also things it should warn about but does not.

• Attach line number information to syntax trees during parsing so that Cozy's error messages can show location information
• Identifiers may not start with underscores (Cozy generates fresh names by prefixing them with _)
• Taking the min or max of an empty collection.
• Boolean expressions that are always true or always false. (These can be caused by developer mistakes or by the limitations of bounded verification.)
• String literals are not fully supported (See Solver cannot deal with string literals #20)
• No two functions (query specifications or extern functions) may have the same name (This is a defensive measure that protects against bugs in the rest of Cozy.)
• Two arguments to a function cannot have the same name (This is a defensive measure that protects against bugs in the rest of Cozy.)
• Two state variables cannot have the same name (This is a defensive measure that protects against bugs in the rest of Cozy.)
• No function argument may have the same name as a state variable (This is a defensive measure that protects against bugs in the rest of Cozy.)
• If a method calls a query, it must satisfy that query's preconditions where the call is made
• you are not allowed to remove missing elements from a bag or set
• all arguments mentioned in the definitions of extern functions should be actual arguments to the function
• all abstract state variables should be read by some query or update operation

[izgzhen]

https://github.com/CozySynthesizer/cozy/search?q=lineno&unscoped_q=lineno @sureyeaah this might be useful to you