Skip to content
Snippets Groups Projects
Commit de7db426 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] don't use additional header for exposing generated variables

parent d504d374
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
headers/header_spec.txt
+ 0
− 1
View file @ de7db426
......@@ -208,7 +208,6 @@ share/libc/__fc_runtime.c: CEA_LGPL
share/libc/__fc_select.h: CEA_LGPL
share/libc/__fc_string_axiomatic.h: CEA_LGPL
share/libc/alloca.h: CEA_LGPL
share/libc/aorai/aorai.h: CEA_LGPL
share/libc/arpa/inet.h: CEA_LGPL
share/libc/assert.c: CEA_LGPL
share/libc/assert.h: CEA_LGPL
......
share/libc/aorai/aorai.h deleted 100644 → 0
+ 0
− 33
View file @ d504d374
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2020 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
#ifndef __FC_AORAI
#define __FC_AORAI
/*@ ghost extern int aorai_CurStates; */
/*@ ghost extern int aorai_StatesHistory1; */
/*@ ghost extern int aorai_StatesHistory2; */
/*@ ghost extern int aorai_StatesHistory3; */
/*@ ghost extern int aorai_StatesHistory4; */
#endif
src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+ 23
− 23
View file @ de7db426
[kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning:
[kernel:typing:implicit-function-declaration] tests/ya/serial.c:79: Warning:
Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel:annot:missing-spec] tests/ya/serial.c:45: Warning:
[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
......@@ -21,28 +21,28 @@
aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval
[eva] tests/ya/serial.c:47: starting to merge loop iterations
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
[eva:alarm] tests/ya/serial.c:54: Warning:
[eva] tests/ya/serial.c:45: starting to merge loop iterations
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
[eva:alarm] tests/ya/serial.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&status);
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
[aorai] tests/ya/serial.c:81: Error <- Error <- Error
[aorai] tests/ya/serial.c:81: Error <- Error <- Error
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2100 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
......
src/plugins/aorai/tests/ya/serial.c
+ 0
− 2
View file @ de7db426
......@@ -3,8 +3,6 @@
*/
#include "__fc_builtin.h"
#include "aorai/aorai.h"
/*@ assigns \result \from \nothing;
ensures 0 <= \result < 0x100; */
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment