diff --git a/tests/misc/asm_initialized.i b/tests/misc/asm_initialized.i new file mode 100644 index 0000000000000000000000000000000000000000..2932eef91d330df13b5a880c8687a4bff476c1c3 --- /dev/null +++ b/tests/misc/asm_initialized.i @@ -0,0 +1,12 @@ +/* run.config* +PLUGIN: @EVA_PLUGINS@ +STDOPT: #"-asm-contracts-ensure-init -print" +*/ + +int main() { + int* sp; + int x; + asm volatile ("mov %%rsp, %0;":"=r"(sp)); + *(sp - 2) = 3; + return x; +} diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..dd13230b7df0c57d2ece51de371ff102b989112b --- /dev/null +++ b/tests/misc/oracle/asm_initialized.res.oracle @@ -0,0 +1,45 @@ +[kernel] Parsing asm_initialized.i (no preprocessing) +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva:initial-state] Values of globals at initialization + +[eva:alarm] asm_initialized.i:10: Warning: + accessing uninitialized left-value. assert \initialized(&sp); +[eva:alarm] asm_initialized.i:10: Warning: + out of bounds write. assert \valid(sp - 2); +[kernel] asm_initialized.i:10: Warning: + all target addresses were invalid. This path is assumed to be dead. +[eva] Recording results for main +[eva] Done for function main +[eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function main: + NON TERMINATING FUNCTION +[from] Computing for function main +[from] Non-terminating function main (no dependencies) +[from] Done for function main +[from] ====== DEPENDENCIES COMPUTED ====== + These dependencies hold at termination for the executions that terminate: +[from] Function main: + NON TERMINATING - NO EFFECTS +[from] ====== END OF DEPENDENCIES ====== +[inout] Out (internal) for function main: + \nothing +[inout] Inputs for function main: + \nothing +/* Generated by Frama-C */ +int main(void) +{ + int *sp; + int x; + /*@ ensures \initialized(&sp); + assigns sp; + assigns sp \from \nothing; */ + __asm__ volatile ("mov %%rsp, %0;" : "=r" (sp)); + /*@ assert Eva: initialization: \initialized(&sp); */ + /*@ assert Eva: mem_access: \valid(sp - 2); */ + *(sp - 2) = 3; + return x; +} + +