Activity for Frederic Rioux
-
Frederic Rioux committed [r862]
The unary and binary promotion methods of CNumericType have been changed from class methods to instance methods. This change is necessary to support the new JML promotion process (that deals with \bigint and \real). Changes in support of feature #738013.
-
Added Lexer support for "bigint" and "real" (implementation of task 78319)
-
Preliminary work in support of implicit promotion to \bigint (part of feature #738013).
-
[Feature 738013]
-
[Feature 738013] Added factory methods for the creation of (a preliminary set) of arithmetic expressions. This will allow us to leave the Mjc grammar untouched while creating appropriate AST nodes (Mjc or Jml specific). Also refactored the unary and binary promote methods of CNumericType.
-
Added support for the "safe" arithmetic for the binary subtraction, division and multiplication.
-
[Feature 738013]
-
Minor changes to enable JMLb support in JML. Also, previously commented methods were permanently removed.
-
Addition of a mechanism to check the arithmetic mode. Soon, the "--safemath" option of MJ will be refactored to use that mechanism which will also be used in JML to implement JMLb (see the post on jml-developers of July 30 for further details)
-
Added needed support to make the arithmetic mode operators work in JML. This also enables MJ to use arithmetic mode operators in the future (given that they are added in the grammar).
-
Replacement of the old integer overflows checking mechanism by a new one supporting more than two arithmetic mode. This feature is needed for the implementation of JMLb.
-
Rework was done on the math modes in MJ and JML to allow the compiler/checker to issue warnings if an unsafe arithmetic operation can potentially overflow in the default math mode of a specification. In its current version, the warnings are turned off by default and only the unary minus and binary addition are handled. The future version of this feature will handle all unsafe operations and the warnings will be turned on by default.
-
Refactored the math modes in MJ and JML to allow the compiler/checker to issue warnings if an unsafe arithmetic operation can potentially overflow in the default math mode of a specification. In its current version, the warnings are turned off by default and all unsafe operators are handled. In the future version of this feature, the warnings will be turned on by default.
-
replaced null annotations by nullable annotations (due to experimental feature keyword change in JML)
-
Added some JML annotations
-
Added some JML annotations
-
Added some JML specifications
-
Added some JML specifications
-
Added some JML specifications
-
Test cases for the Lexer support for "bigint" and "real" (implementation of task 78319)
-
Added Lexer support for "bigint" and "real" (implementation of task 78319)
-
Added support for the JML primitive \bigint and \real (part of feature #738013).
-
Ensured jmldoc support of the JML primitive \bigint and \real (part of feature #738013).
-
Updated a testcase expected output for \bigint (part of feature #738013).
-
Preliminary work in support of implicit promotion to \bigint (part of feature #738013).
-
Removed an unneeded functions, line breaks, and call to super class.
-
Changed the end of line character to a Unix standard. This corrected a portability problem when testing on a Window machine.
-
The unary and binary promotion methods of CNumericType have been changed from class methods to instance methods. This change is necessary to support the new JML promotion process (that deals with \bigint and \real). Changes in support of feature #738013.
-
[Feature 738013] Added factory methods for the creation of (a preliminary set) of arithmetic expressions. This will allow us to leave the Mjc grammar untouched while creating appropriate AST nodes (Mjc or Jml specific).
-
[Feature 738013] Added factory methods for the creation of (a preliminary set) of arithmetic expressions. This will allow us to leave the Mjc grammar untouched while creating appropriate AST nodes (Mjc or Jml specific). Also refactored the unary and binary promote methods of CNumericType.
-
[Feature 738013]
-
[Feature 738013]
-
[Feature 738013]
-
Added support for \warn, \nowarn, \warn_op, \nowarn_op by adding the expressions in the grammar of JML and reserving the keyword.
-
Added support for the "safe" arithmetic for the binary subtraction, division and multiplication.
-
Addition of temporary fixes to IntMathOps* files needed because the implementation of \bigint in the RAC is not fully supported (i.e. \bigint's are approximated by long's). Hence, RAC generated code was looking for JMLMath.abs(long) ... which does not exist.
-
Temporary fix: removed a testing value that caused a failure because the implementation of \bigint in the RAC is not fully supported.
-
Partial implementation of JMLb support in the JML checker. The mechanism to access and modify the mode was implemented in the contexts.
-
Partial implementation of JMLb support in the JML checker.
-
New implementation of JMLa using the mechanisms that will be used for JMLb (i.e. the version of JML with multiple arithmetic modes).
-
Added the artihmetic mode operators (part of the implementation of JMLb)
-
Implementation of the support for JMLb. Currently, the java_math and safe_math modes are supported for both code and specification. Also, the bigint_math mode is supported for specification.
-
Refactored the math modes in MJ and JML to allow the compiler/checker to issue warnings if an unsafe arithmetic operation can potentially overflow in the default math mode of a specification. In its current version, the warnings are turned off by default and all unsafe operators are handled. In the future version of this feature, the warnings will be turned on by default.
-
Rework was done on the math modes in MJ and JML to allow the compiler/checker to issue warnings if an unsafe arithmetic operation can potentially overflow in the default math mode of a specification. In its current version, the warnings are turned off by default and only the unary minus and binary addition are handled. The future version of this feature will handle all unsafe operations and the warnings will be turned on by default.
-
Fixed the checker's test cases so that when the unsafe operation warnings will be turned on by default, none of those tests will fail. Also corrected a bug
-
Fixed a null pointer dereference that occured when computing the non_null statistics
-
Added some JML annotations
-
Added some JML annotations
-
Added some JML specifications
-
Added some JML specifications
-
Added missing method declarations so that the diff test passes
-
Added missing imports in java.sql specs
-
new version of the specs for servlets
-
removed old version of the specs
-
Added missing method signatures to java.sql specs
-
refactored constants name to reflect new keyword names
-
modified some experimental feature keywords (e.g. null -> nullable, non_null_ref_by_default -> non_null_by_default, null_ref_by_default -> nullable_by_default)
-
corrected a grammar rule (null -> nullable)
-
fixed a typo
-
added post-condition support
-
rename a target so that the tests run when runtests is called
-
Initial release of an alternative way of evaluating expressions in the RAC. The option is currently turned off by default, and since the feature is not fully implemented, it should not be used. Development of that feature should be completed and properly documented by the end of the year.
-
removed a specification that caused trouble with jmldoc
-
Fixed dynamic method call translation for the alternative expression translation (experimental feature)
-
Added bigint handling, several bugfixes, and refactoring for the alternative expression translation (experimental)
-
removed debug messages that were displayed by default when using the -T option.
-
further updates to the experimental alternative translation mechanism
-
Further improvements on the alternative expression translation (experimental feature)
-
added missing visitor methods
-
Improved the use of error and warnings for the alternative translation (experimental)
-
Added missing exception classes
-
better support for fields translation (experimental alternative RAC expression translation)
-
Fixed a possible null pointer dereference occurance
-
bug fixes for the alternative RAC expression translation (experimental)
-
Added exceptional post-condition support for the alternative expression translation (experimental feature)
-
Fixed error reporting message for alternative expression translation (experimental)
-
Removed the old grep-based (and already disabled) testing strategy for the alternative expression translation (experimental feature)
-
Further improvement in alternative expression translation (experimental feature)
-
Further improvements on the alternative expression translations (experimental feature)
-
Further work on the alternative expression translation (experimental feature)
-
Added quantified expression support and new test harness (disabled for the moment) for the alternative RAC expression translation [experimental feature]
-
Further work on the alternative expression translation (experimental feature). Fixed the ThisExpression bug and the nested quantifiers with pre-state values. Also modified some tests. Test suite is still disabled by default.
-
enabled test harness for alternative expression translation (experimental)
-
fixed a copy-paste error which resulted in one test being run twice, and one not being run at all
-
Fixed a possible variable redefinition
-
Fixed a bigint cast problem and the way to deal with this from within inner anonymous classes
-
Improved the handling of quantified statements for the alternative expression translation (experimental). Also worked on the tests.
-
Added dropped clauses truth value switching mechanism for the alternative expression translation (experimental)
-
Merged the new semantics rac testcases (racalt) into the general (racrun) rac test folder. Racalt will be completely removed soon.
-
Modified the error hierarchy to have the evaluation error report the type of clause that failed (alternative RAC semantics)
-
Renamed JMLRacExpressionEvaluationError to JMLEvaluationError
-
Fixed bug 1746834 (min, max, and num_of in new Rac semantics)
-
Fixed a tabulation that had been replaced by 8 spaces by mistake
-
moved the evaluation of the old expressions from before to after the evaluation of the precondition and implicit nullity checks
-
Fixed a problem that had the new semantics tests run twice and the old semantics tests never run
-
Removed old test cases that have been merged into the racrun package (i.e. the same testcases are used for testing both semantics now)
1