Commit d496a077 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

synchronize with frama-c master

parent ca79eed7
Pipeline #36347 passed with stage
in 57 minutes and 21 seconds
directory file line function property kind status property
. provenance_via_io_auto.c 11 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_auto.c 19 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 429 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 436 rewind precondition Unknown valid_stream: \valid(stream)
directory file line function property kind status property
. provenance_via_io_global.c 10 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_global.c 18 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 429 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 436 rewind precondition Unknown valid_stream: \valid(stream)
directory file line function property kind status property
. provenance_via_io_percentp_global.c 9 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_percentp_global.c 16 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 429 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 436 rewind precondition Unknown valid_stream: \valid(stream)
directory file line function property kind status property
. provenance_via_io_uintptr_t_global.c 10 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_uintptr_t_global.c 18 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 429 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 436 rewind precondition Unknown valid_stream: \valid(stream)
......@@ -817,8 +817,8 @@ FRAMAC_SHARE/libc stdio.h 217 sscanf_va_8 precondition Unknown valid_read_string
FRAMAC_SHARE/libc stdio.h 217 sscanf_va_9 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 288 fputs precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 351 fread precondition Unknown valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
FRAMAC_SHARE/libc stdio.h 551 popen precondition Unknown valid_command: valid_read_string(command)
FRAMAC_SHARE/libc stdio.h 566 pclose precondition Unknown open_pipe: is_open_pipe(stream)
FRAMAC_SHARE/libc stdio.h 558 popen precondition Unknown valid_command: valid_read_string(command)
FRAMAC_SHARE/libc stdio.h 573 pclose precondition Unknown open_pipe: is_open_pipe(stream)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc string.c 130 strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 130 strcmp mem_access Unknown \valid_read(s1 + i)
......
Subproject commit 7562208af674d75b4cdd8db615ec3236f6405f2d
Subproject commit ab43a5ed6ba8a5975fa70813fdfa96d1f20586d7
......@@ -643,8 +643,8 @@ FRAMAC_SHARE/libc stdio.h 207 fprintf_va_73 precondition Unknown valid_read_stri
FRAMAC_SHARE/libc stdio.h 211 printf_va_8 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 266 fgets precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 323 putc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 447 fileno precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 477 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 454 fileno precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 484 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdlib.c 45 atoi mem_access Unknown \valid_read(up)
FRAMAC_SHARE/libc stdlib.c 47 atoi mem_access Unknown \valid_read(up)
FRAMAC_SHARE/libc stdlib.c 53 atoi mem_access Unknown \valid_read(up)
......
util.c:186:[eva:garbled-mix] warning: The specification of function strrchr has generated a garbled mix for assigns clause \result.
util.c:400:[eva] warning: ignoring unsupported \allocates clause
FRAMAC_SHARE/libc/signal.h:116:[eva] warning: no 'assigns \result \from ...' clause specified for function signal
FRAMAC_SHARE/libc/signal.h:122:[eva] warning: no 'assigns \result \from ...' clause specified for function signal
gzip.c:646:[kernel:annot:missing-spec] warning: Neither code nor specification for function fstat, generating default assigns from the prototype
inflate.c:403:[eva] warning: ignoring unsupported \allocates clause
inflate.c:412:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
......
directory file line function property kind status property
FRAMAC_SHARE/libc stdio.h 207 fprintf assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 from clause Unknown assigns \result \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 from clause Unknown assigns *stream \from *stream, *(format + (0 ..)), param0, param1, param2, param3, param4;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 from clause Unknown assigns \result \from *stream, *(format + (0 ..)), param0, param1, param2, param3, param4;
src impls.c 96 Sleep signed_overflow Unknown _t + delayMs ≤ 2147483647
......@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
433 stmts in analyzed functions, 415 stmts analyzed (95.8%)
424 stmts in analyzed functions, 406 stmts analyzed (95.8%)
Interpolate_from_curve: 15 stmts out of 15 (100.0%)
Limiter_out: 6 stmts out of 6 (100.0%)
Ramp_getDir: 2 stmts out of 2 (100.0%)
......@@ -20,7 +20,7 @@ Timer_elapsedTime: 2 stmts out of 2 (100.0%)
Timer_start: 2 stmts out of 2 (100.0%)
Timer_tick: 2 stmts out of 2 (100.0%)
Turn_on_delay: 8 stmts out of 8 (100.0%)
main: 51 stmts out of 51 (100.0%)
main: 42 stmts out of 42 (100.0%)
Ramp_out: 22 stmts out of 23 (95.7%)
RoCo_process: 213 stmts out of 229 (93.0%)
PT1_Filter: 5 stmts out of 6 (83.3%)
src/main.c:33:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
src/main.c:33:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf_fallback_1, generating default assigns from the prototype
src/main.c:41:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf_fallback_2, generating default assigns from the prototype
......@@ -752,6 +752,12 @@ void Sim_init(void)
char *output_header =
(char *)"time(ms)\tengineVoltage\tlegAngle\tlegAngleValid\tisActive\n";
char *output_row_fmt_string = (char *)"%d\t%f\t%f\t%d\t%d\n";
int fprintf_fallback_1(FILE * restrict stream, char const * restrict format);
int fprintf_fallback_2(FILE * restrict stream, char const * restrict format,
sint32 param0, real64 param1, real64 param2,
int param3, int param4);
int main(void)
{
int __retres;
......@@ -766,11 +772,7 @@ int main(void)
RoCo_activeDesired = (char)1;
RoCo_moveFast = (char)0;
int cnt = 0;
{
void *__va_args[1] = {(void *)0};
fprintf(__fc_stderr,(char const *)output_header,
(void * const *)(__va_args));
}
fprintf(__fc_stderr,(char const *)output_header); /* fprintf_fallback_1 */
while (cnt < 9000) {
sint32 tmp_0;
tmp_0 = Time();
......@@ -778,19 +780,10 @@ int main(void)
lastTime = Time();
RoCo_process();
Sim_process();
if (cnt % 5 == 0) {
{
sint32 __va_arg0 = lastTime;
real64 __va_arg1 = RoCo_engineVoltage;
real64 __va_arg2 = RoCo_legAngle;
int __va_arg3 = (int)RoCo_legAngleValid;
int __va_arg4 = (int)RoCo_isActive;
void *__va_args_12[5] =
{& __va_arg0, & __va_arg1, & __va_arg2, & __va_arg3, & __va_arg4};
fprintf(__fc_stderr,(char const *)output_row_fmt_string,
(void * const *)(__va_args_12));
}
}
if (cnt % 5 == 0) fprintf(__fc_stderr,
(char const *)output_row_fmt_string,lastTime,
RoCo_engineVoltage,RoCo_legAngle,
(int)RoCo_legAngleValid,(int)RoCo_isActive); /* fprintf_fallback_2 */
Sleep(20);
cnt ++;
if (cnt == 2500) {
......
......@@ -26,13 +26,13 @@ Potential entry points (3)
Global metrics
==============
Sloc = 437
Sloc = 428
Decision point = 100
Global variables = 98
If = 100
Loop = 2
Goto = 13
Assignment = 243
Assignment = 236
Exit point = 18
Function = 18
Function call = 42
......
......@@ -38,6 +38,6 @@ Function main calls G (at 2019/duble/prog.c:63)
Function main calls G (at 2019/duble/prog.c:64)
[metrics] Statements analyzed by Eva
--------------------------
304 stmts in analyzed functions, 4 stmts analyzed (1.3%)
302 stmts in analyzed functions, 4 stmts analyzed (1.3%)
P: 2 stmts out of 4 (50.0%)
main: 2 stmts out of 300 (0.7%)
main: 2 stmts out of 298 (0.7%)
......@@ -295,6 +295,8 @@ struct termios o;
int printf_va_1(char const * restrict format, char *param0, int param1,
char *param2);
int printf_fallback_1(char const * restrict format);
/*@ requires valid_read_nstring(param2, 11);
requires valid_read_string(param7);
requires valid_read_string(param8);
......@@ -557,10 +559,7 @@ int main(int F_0, char **D_0)
}
}
}
{
void *__va_args[1] = {(void *)0};
printf((char const *)I,(void * const *)(__va_args));
}
printf((char const *)I); /* printf_fallback_1 */
break;
}
}
......
......@@ -21,13 +21,13 @@ Potential entry points (1)
Global metrics
==============
Sloc = 373
Sloc = 371
Decision point = 74
Global variables = 33
If = 74
Loop = 9
Goto = 2
Assignment = 182
Assignment = 181
Exit point = 8
Function = 8
Function call = 63
......
......@@ -253,6 +253,8 @@ void d(void)
return;
}
int printf_fallback_1(char const * restrict format, P param0);
void R(void)
{
int tmp_1;
......@@ -262,11 +264,7 @@ void R(void)
D = & j[*(i + 2)];
tmp = U((unsigned int)1);
if (E) tmp_0 = "%c"; else tmp_0 = "%u,";
{
P __va_arg0 = tmp;
void *__va_args[1] = {& __va_arg0};
tmp_1 = printf(tmp_0,(void * const *)(__va_args));
}
tmp_1 = printf(tmp_0,tmp); /* printf_fallback_1 */
tmp_2 = w((unsigned int)2);
*D = l(tmp_2,(unsigned int)tmp_1);
D ++;
......
......@@ -29,13 +29,13 @@ Potential entry points (1)
Global metrics
==============
Sloc = 324
Sloc = 321
Decision point = 22
Global variables = 13
If = 22
Loop = 5
Goto = 0
Assignment = 196
Assignment = 194
Exit point = 26
Function = 26
Function call = 66
......
......@@ -101,5 +101,5 @@ FRAMAC_SHARE/libc stdio.h 120 fclose precondition Unknown valid_stream: \valid(s
FRAMAC_SHARE/libc stdio.h 150 fopen precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 258 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 281 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 477 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 484 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdlib.h 564 abs precondition Unknown abs_representable: j > -2147483647 - 1
......@@ -85,5 +85,5 @@ FRAMAC_SHARE/libc stdio.h 120 fclose precondition Unknown valid_stream: \valid(s
FRAMAC_SHARE/libc stdio.h 150 fopen precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 258 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 281 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 477 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 484 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdlib.h 564 abs precondition Unknown abs_representable: j > -2147483647 - 1
Markdown is supported
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