The information below is specific to the C problems. Monitoring specific C problem properties

The C implementations of the program come as a single C source file. For maximum compatibility with existing software model checking tools, the only data type which is used is int (or int arrays). Since input and outputs are expected as (one-letter) strings, the translation is realized by replacing letters by their position in the latin alphabet: "A" is replaced by 1, "X" by 24 and so on. At the top of each source file, the valid input symbols are explicitly listed in an array along with all errors than can occur.

	// inputs
	int inputs[] = {3,1,6,5,2,4};
	const int error_0 = 1;
	const int error_1 = 1;
	...

The program's logic is contained in a method called calculate_output, which is a sequence of nested if-then-else blocks. The state of the program is maintained in a set of attributes.

    int calculate_output(int input)
    {
        if(input == 3                              
            && (a7 != 0 && a0 == 9 && a6 == 0))	   		
        {
            a3 = a5[a4 + 6];                                 
            a9 = 2;
            printf("%d\n", 24); fflush(stdout); 
        }
        ...
     }

At the bottom of this function, a method errorCheck is called that checks in a sequence of if-statements whether the system is in an invalid state. If this is the case, an error is raised by a failed assertion. To identify the specific error in the source code, the assertion is labeled with the error ID. On execution of the compiled file, the error label will also be printed to the console.

    int calculate_output(int input) {
        ...
        if((a23 == 0 && a3 != 0 && a26 == 3))
error_6: 	assert(!error_6);
        ...
    }

The main() function, which is also contained in the source file, consists of the main loop which connects the program to continuous inputs (via stdin) and eventually leads to outputs (via stdout).

int main()
{
    // main i/o-loop
    while(1)
    {
        // read input
        int input;
        scanf("%d", &input);        

        // operate eca engine
        calculate_output(input);
    }
}

The systems can be compiled using gcc and executed without any prerequisites.

    $ gcc -o ProblemX ProblemX.c 
    $ ./ProblemX
    1                                   
    24                                   
    .
    .
    .

---

Each monitoring C file contains method definitions for methods implemented in the ProblemXExternal.c file.

int check69(int v);

At some points in the text variables in the external file are updated or their values checked for certain values. The outcome of these checks influences the behaviour of the system. ProblemXExternal.java will be replaced at a later point in the challenge, so you have access to the real system behaviour. Please read the rules page for further information.

check69(10)

The systems can be compiled using gcc and executed using without any prerequisites.

    $ gcc -o ProblemX ProblemX.c ProblemXExternal.c
    $ ./ProblemX 
    1                                   
    24                                   
    .
    .
    .