gpetiot / frama-c-stady Goto Github PK
View Code? Open in Web Editor NEWStatic & Dynamic Verification of C programs
License: GNU Lesser General Public License v3.0
Static & Dynamic Verification of C programs
License: GNU Lesser General Public License v3.0
I try to find a counter example for the assertion at the end of function relational_wrapper_1:
Rpp: return_variable_relational_1 == - return_variable_relational_2;
I get message reporting Invalid memory reference.
However, if I try to find counter example for a rewritten version, everything goes well:
Rpp: return_variable_relational_1 == 0 - return_variable_relational_2;
struct CollectionItem {
int cardSet ;
int cardRarity ;
int cardId ;
int cardType ;
};
void relational_wrapper_1(struct CollectionItem x1, struct CollectionItem x2)
{
int return_variable_relational_1;
int return_variable_relational_2;
{
int __retres_1;
if (x1.cardSet < x2.cardSet) {
__retres_1 = -1;
goto return_label_label_1;
}
else {
if (x1.cardSet == x2.cardSet)
if (x1.cardRarity < x2.cardRarity) {
__retres_1 = 1;
goto return_label_label_1;
}
else {
if (x1.cardId == x2.cardId)
if (x1.cardType > x2.cardType) {
__retres_1 = 1;
goto return_label_label_1;
}
else {
if (x1.cardType == x2.cardType) {
__retres_1 = 0;
goto return_label_label_1;
}
__retres_1 = -1;
goto return_label_label_1;
}
__retres_1 = -1;
goto return_label_label_1;
}
__retres_1 = 1;
goto return_label_label_1;
}
return_label_label_1: return_variable_relational_1 = __retres_1;
}
{
int __retres_2;
if (x2.cardSet < x1.cardSet) {
__retres_2 = -1;
goto return_label_label_2;
}
else {
if (x2.cardSet == x1.cardSet)
if (x2.cardRarity < x1.cardRarity) {
__retres_2 = 1;
goto return_label_label_2;
}
else {
if (x2.cardId == x1.cardId)
if (x2.cardType > x1.cardType) {
__retres_2 = 1;
goto return_label_label_2;
}
else {
if (x2.cardType == x1.cardType) {
__retres_2 = 0;
goto return_label_label_2;
}
__retres_2 = -1;
goto return_label_label_2;
}
__retres_2 = -1;
goto return_label_label_2;
}
__retres_2 = 1;
goto return_label_label_2;
}
return_label_label_2: return_variable_relational_2 = __retres_2;
}
/*@ assert
Rpp: return_variable_relational_1 == - return_variable_relational_2;
*/
return;
}
I have the following error for the example issue.c
give as an attachment:
[kernel] Parsing issue.c (with preprocessing)
[kernel] Current source was: issue.c:28
The full backtrace is:
Raised at file "translate.ml", line 876, characters 19-30
Called from file "translate.ml", line 900, characters 13-24
Called from file "translate.ml", line 908, characters 20-60
Called from file "translate.ml", line 920, characters 11-65
Called from file "translate.ml", line 924, characters 21-34
Called from file "translate.ml", line 985, characters 34-56
Called from file "list.ml", line 77, characters 12-15
Called from file "translate.ml", line 992, characters 4-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml", line 3723, characters 5-91
Called from file "src/kernel_services/ast_queries/cil.ml", line 3814, characters 16-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml", line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "src/kernel_services/visitors/visitor.ml", line 849, characters 28-60
Called from file "register.ml", line 102, characters 4-60
Called from file "register.ml", line 142, characters 6-21
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 15-18
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (StaDy.Translate.Unreachable).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
I try to find counter examples for the assert clause in the relational_wrapper_1 function in
the test.c file in Example.zip.
The instrument file generated by Stady is also placed in the .zip
I get the following back trace:
[kernel] Parsing test.c (with preprocessing)
[kernel] Parsing __sd_instru_test_relational_wrapper_1.c (with preprocessing)
[kernel] Parsing __sd_instru_test_relational_wrapper_1.c (with preprocessing)
[pc] Starting lanceur_relational_wrapper_1 (isc version)
[pc] Starting lanceur_pathcrawler__relational_wrapper_1_precond (isc version)
[pc] Starting lanceur_relational_wrapper_1 (isc version)
[pc] TEST GENERATION WARNING!!!
[pc] Bad projection on input values of expression return_variable_relational_1__relational_wrapper_1 in the assignment at line number 282 of file __sd_instru_test_relational_wrapper_1.c.
[pc] Please check your test context and source code for uninitialised variables.
[pc] Starting lanceur_relational_wrapper_1 (isc version)
[pc] Unexpected exception occured: Sys.Break
Raised at file "sys.ml", line 102, characters 52-57
Called from file "unix.ml", line 862, characters 6-20
Called from file "unix.ml", line 862, characters 6-20
Called from file "unix.ml", line 874, characters 13-34
Called from file "pc_scripts.ml", line 701, characters 4-19
Called from file "pc_scripts.ml", line 758, characters 6-22
[stady] user error: internet socket now closed!
[kernel] Plug-in stady aborted: invalid user input.
It would be interesting to have a support for variables with several offset in ensures
clauses.
The following example make Stady crach :
struct s{
int t[10];
};
/*@ ensures \result == a.t[0];*/
int f(struct s a){
return a.t[0];
}
void main(struct s a){
int b;
b = f(a);
/*@ assert b == a.t[1];*/
}
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.