Permalink
Commits on Mar 28, 2012
Commits on Mar 27, 2012
Commits on Mar 16, 2012
  1. [z3model] Nicely format function variables and ternary cascades

    Function variables (variables that represent the return value of a function)
    are now nicely printed with the function's name and source location.
    
    Some cascades of ternary expressions are now transformed into array function
    accesses.
    jspam committed Mar 16, 2012
  2. [z3model] Update model with let and ternary expressions

    These are required by the Z3 model parser. Also add some special
    handling when generating string representation of the Z3 model.
    jspam committed Mar 16, 2012
Commits on Mar 14, 2012
Commits on Mar 12, 2012
  1. Fix frame title and uncover hidden lines in listing

    - do not change frame title for syntax example in between
    - do not change number of lines shown in transformation listing
    bafain committed Mar 12, 2012
  2. [abschluss] Correct minor issues in presentation

     - Use Z instead of N for integer numbers
     - Wrap "<" operator in math mode to ensure same look as "<="
     - Syntax-highlight "if" statement
    jspam committed Mar 12, 2012
Commits on Mar 11, 2012
  1. Add test program array_min

    bafain committed Mar 11, 2012
Commits on Mar 10, 2012
  1. Fix checkstyle errors in (Grammar|Validator)Test

    - make Test classes final
    - remove unused import
    - add missing javadoc
    - apply Worthwhile formatter
    bafain committed Mar 10, 2012
  2. Move testReturnStatementOnlyFunction to GrammarTest

    Since 65871cc ReturnStatements are
    linked to the FunctionDeclaration they belong to by the parser so that
    in case a `return' occurs outside a function declaration the parser
    already reports an error and ValidatorTest would fail requiring test
    programs to have correct syntax.
    bafain committed Mar 10, 2012
  3. Fix return value variables are bound in the wrong order

    - this commit amends 8b622f5
    bafain committed Mar 10, 2012
  4. [prover] Add macro substitution for simple postconditions

    If the postcondition of a function is "simple", i.e. of the form
    "_ensures _return = XYZ", we can replace a function call by the ensured
    return value XYZ.
    
    This avoids cluttered formulas when using helper functions.
    
    The macro substitution is applied before the function call substitution
    which substitutes all leftover function calls. However, the preconditions
    need to be asserted in both cases. This functionality has been placed
    in a special FunctionCallPreconditionAssertion class.
    jspam committed Mar 9, 2012
  5. Insert division by zero in loop condition guard as invariant

    - the division by zero in loop condition guard is no more added as
      assertion since the inserted invariant implies it
    bafain committed Mar 10, 2012
  6. Set actualValidity in RunProgramTest on expressionFailed

    - this overrides the default behaviour of throwing a RuntimeException
      which can both be expected and not as test result, so set
      actualValidity to indicate whether the execution failed or not
    bafain committed Mar 10, 2012