C Programs - Revision history

Ffrohn: /* Proposed semantics */

2025-08-19T14:41:35Z

Proposed semantics

Cryingshadow: format fix

2015-07-29T15:05:26Z

format fix

Cryingshadow: formatting

2015-07-29T15:04:54Z

formatting

Cryingshadow: new rules according to discussion on termtools

2015-07-29T15:00:22Z

new rules according to discussion on termtools

Cryingshadow at 11:13, 2 July 2014

2014-07-02T11:13:12Z

Albert: /* Proposed semantics */

2014-05-26T10:42:27Z

Proposed semantics

Albert: /* Discussion */

2014-05-26T10:40:12Z

Discussion

J.waldmann at 10:38, 14 May 2014

2014-05-14T10:38:43Z

J.waldmann: Created page with "== Proposed semantics == * The starting point is the main function without arguments. * Functions which are only declared, but not defined, are considered to be termin..."

2014-05-14T10:18:06Z

Created page with "== Proposed semantics == * The starting point is the main function without arguments. * Functions which are only declared, but not defined, are considered to be termin..."

New page

== 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.

* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and we have to decide upon the handling of wrong answers in the same way for all categories).

* time limit: 300 seconds

== Discussion ==

* proposed time limit (5 min) is between the limits used in SV-COMP (15 min) and termcomp (1 min)

== See also ==

Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

← Older revision		Revision as of 14:41, 19 August 2025
Line 8:		Line 8:

	* 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).		* 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).
		+
		+	* The function exit(int) terminates the execution of the program.

	* 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.		* 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.

@@ Line 32: / Line 32: @@
       while( x++ == x );
+  }
-: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code><P></code> where the execution of <code>gcc -c -std=c99 -Wsequence-point <P></code> shows a warning.
+: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code>P</code> where the execution of <code>gcc -c -std=c99 -Wsequence-point P</code> shows a warning.
 *    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).

@@ Line 28: / Line 28: @@
 *    Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program
   int main(){
       int x = 0;
       while( x++ == x );
+  }
+: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code><P></code> where the execution of <code>gcc -c -std=c99 -Wsequence-point <P></code> shows a warning.
 *    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).

@@ Line 7: / Line 7: @@
 *    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)
+*    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.
@@ Line 13: / Line 13: @@
 *    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.
+*    Integer division by negative numbers is assumed to be done by truncation towards zero (as in the C99 standard and no implementation-defined behavior as in the C89 standard).
 *    We assume the following sizes of primitive data types:
@@ Line 25: / Line 27: @@
       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).
+*    Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program
-* time limit: 300 seconds
+*    Time limit: 300 seconds.
 == See also ==
 Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

← Older revision		Revision as of 11:13, 2 July 2014
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).

← Older revision		Revision as of 10:38, 14 May 2014
Line 1:		Line 1:
		+	[[Category:Categories]]
		+
	== Proposed semantics ==		== Proposed semantics ==