--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2017 ---
Hi All, I was playing around with the impact analysis with the following example: I have two variables conf_data and nonconf_data and I am tagging the assignment to the former. I was expecting to see the call to and definition of harmlessFunction() in the results but I get the following, which contains the assignment to nonconf_data and its use. Could someone explain to me why they get included? The command I am running is commented out at the beginning of the code. [impact] impacted statements of stmt(s) 26 are: test-pointer-constraints.c:14 (sid 4): val = *array_D; test-pointer-constraints.c:15 (sid 6): return val; test-pointer-constraints.c:24 (sid 13): tmp = verboseLog(array_C); test-pointer-constraints.c:24 (sid 14): return tmp; test-pointer-constraints.c:34 (sid 26): *(conf_data + i) = Frama_C_interval (0,9); * test-pointer-constraints.c:38 (sid 34): *(nonconf_data + i) = Frama_C_interval* * (0,9);* * test-pointer-constraints.c:42 (sid 37): val = harmfulFunction(nonconf_data);* test-pointer-constraints.c:63 (sid 48): tmp = main(3,argv); [impact] analysis done ---------------------------------------------------------------------------------------------------- #include <stdio.h> #include <stdlib.h> #include "__fc_builtin.h"/*frama-c -main analysis_main -impact-pragma main test-pointer-constraints.c -val -val-builtins-auto -no-val-malloc-returns-null -context-width 3 -slevel 11 -impact-print > test.log*/int Frama_C_interval(int min, int max); int verboseLog(int * inputArray) { int * array_D = inputArray; int val = *array_D; return val; } int * harmlessFunction(int * array_a) { return array_a; } int harmfulFunction(int * array_B) { int * array_C = array_B; return verboseLog(array_C); } int main(int argc, char ** argv) { int * conf_data = (int *) malloc(sizeof(int) * 10); /* Data is sensitive */ int * nonconf_data = (int *) malloc(sizeof(int) * 10); /* Data is not-sensitive */ int i = 0; for(i=0; i < 10; i++) { //@ impact pragma stmt; *(conf_data + i) = Frama_C_interval(0,9); } for(i=0; i < 10; i++) { *(nonconf_data + i) = Frama_C_interval(0,9); } harmlessFunction(conf_data); int val = harmfulFunction(nonconf_data); return 0; } /* Ignore this function. Fake main for Frama-c */ int analysis_main(void) { char *argv[4]; char arg1[2]; char arg2[2]; arg1[0]='0'; arg1[1]=0; arg2[0]='1'; arg2[1]=0; argv[0]="Analyzed application"; argv[1]=arg1; argv[2]=arg2; argv[3]=NULL; return main(3, argv);} -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170127/c9268a0a/attachment-0001.html>