Difference between revisions of "C Programs"

From Termination-Portal.org
Jump to navigationJump to search
Line 12: Line 12:
  
 
*    We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.
 
*    We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.
 +
 +
*    We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior.
 +
 +
*    We assume the following sizes of primitive data types:
 +
    bool: 8 bit
 +
    char: 8 bit
 +
    short: 16 bit
 +
    int: 32 bit
 +
    long: 64 bit
 +
    float: 32 bit
 +
    double: 64 bit
 +
    pointer: 64 bit
  
 
* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).  
 
* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).  

Revision as of 11:13, 2 July 2014


Proposed semantics

  • The starting point is the main function without arguments.
  • Functions which are only declared, but not defined, are considered to be terminating, have no side effects, and return a non-deterministic value according to the function's return type.
  • The special (and only declared) function __VERIFIER_nondet_String() returns a non-deterministic C String, i.e., a pointer to some freshly allocated memory where the last byte of this allocation is the value '\0' (we may provide a standard implementation for this function, but provers are allowed to hard-code its semantics)
  • In C, memory-unsafe programs can behave arbitrarily. Therefore, neither YES nor NO is a correct result for programs violating memory safety. So a proof of memory safety needs to be part of a termination proof. If there is interest for that, we could also offer an additional category where memory safety can be assumed and where no programs are allowed which might violate memory safety.
  • We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.
  • We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior.
  • We assume the following sizes of primitive data types:
    bool: 8 bit
    char: 8 bit
    short: 16 bit
    int: 32 bit
    long: 64 bit
    float: 32 bit
    double: 64 bit
    pointer: 64 bit
  • The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).
  • time limit: 300 seconds

See also

Section D. of Termination Competition on Software Verification (SV-COMP)