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

[basic-cwe-examples] use size_t for a more definite error in 64-bit machdep

parent fef53ef7
Pipeline #32768 failed with stage
in 40 minutes and 18 seconds
directory file line function property kind status property
. cwe190.c 43 main unsigned_overflow Invalid or unreachable (unsigned long)nresp * sizeof(char *) ≤ 18446744073709551615
. cwe190.c 43 main unsigned_overflow Invalid or unreachable nresp * sizeof(char *) ≤ 18446744073709551615
......@@ -6,8 +6,8 @@ Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
42 stmts in analyzed functions, 32 stmts analyzed (76.2%)
packet_get_long_ok: 6 stmts out of 6 (100.0%)
packet_get_long_problem: 5 stmts out of 5 (100.0%)
packet_get_size_t_ok: 6 stmts out of 6 (100.0%)
packet_get_size_t_problem: 5 stmts out of 5 (100.0%)
packet_get_string: 2 stmts out of 2 (100.0%)
random_long: 1 stmts out of 1 (100.0%)
random_size_t: 1 stmts out of 1 (100.0%)
main: 18 stmts out of 28 (64.3%)
/* Generated by Frama-C */
#include "stdlib.h"
long volatile _rand;
long random_long(void)
size_t volatile _rand;
size_t random_size_t(void)
{
return _rand;
}
long packet_get_long_ok(void)
size_t packet_get_size_t_ok(void)
{
long __retres;
size_t __retres;
int tmp_0;
long tmp;
tmp = random_long();
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 0; else tmp_0 = 123456;
__retres = (long)tmp_0;
__retres = (unsigned long)tmp_0;
return __retres;
}
long packet_get_long_problem(void)
size_t packet_get_size_t_problem(void)
{
long tmp_0;
long tmp;
tmp = random_long();
if (tmp) tmp_0 = 9223372036854775807L / (long)2; else tmp_0 = (long)0;
unsigned long tmp_0;
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 18446744073709551615UL / (unsigned long)2 + (unsigned long)1;
else tmp_0 = (unsigned long)0;
return tmp_0;
}
......@@ -37,28 +38,28 @@ int main(void)
{
int __retres;
char **response;
long nresp = packet_get_long_ok();
if (nresp > (long)0) {
response = (char **)malloc((unsigned long)nresp * sizeof(char *));
size_t nresp = packet_get_size_t_ok();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i = (long)0;
size_t i = (unsigned long)0;
while (i < nresp) {
*(response + i) = packet_get_string((char const *)0);
i ++;
i += (size_t)1;
}
}
free((void *)response);
}
nresp = packet_get_long_problem();
if (nresp > (long)0) {
response = (char **)malloc((unsigned long)nresp * sizeof(char *));
nresp = packet_get_size_t_problem();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i_0 = (long)0;
size_t i_0 = (unsigned long)0;
while (i_0 < nresp) {
*(response + i_0) = packet_get_string((char const *)0);
i_0 ++;
i_0 += (size_t)1;
}
}
free((void *)response);
......
[metrics] Defined functions (5)
=====================
main (0 call); packet_get_long_ok (1 call);
packet_get_long_problem (1 call); packet_get_string (2 calls);
random_long (2 calls);
main (0 call); packet_get_size_t_ok (1 call);
packet_get_size_t_problem (1 call); packet_get_string (2 calls);
random_size_t (2 calls);
Specified-only functions (0)
============================
......
directory file line function property kind status property
. cwe190.c 45 main mem_access Unknown \valid(response + i_0)
. cwe190.c 45 main mem_access Invalid or unreachable \valid(response + i_0)
......@@ -5,9 +5,9 @@ Semantically reached functions = 5
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
42 stmts in analyzed functions, 42 stmts analyzed (100.0%)
main: 28 stmts out of 28 (100.0%)
packet_get_long_ok: 6 stmts out of 6 (100.0%)
packet_get_long_problem: 5 stmts out of 5 (100.0%)
42 stmts in analyzed functions, 39 stmts analyzed (92.9%)
packet_get_size_t_ok: 6 stmts out of 6 (100.0%)
packet_get_size_t_problem: 5 stmts out of 5 (100.0%)
packet_get_string: 2 stmts out of 2 (100.0%)
random_long: 1 stmts out of 1 (100.0%)
random_size_t: 1 stmts out of 1 (100.0%)
main: 25 stmts out of 28 (89.3%)
cwe190.c:45:[nonterm] warning: non-terminating loop
stack: main
cwe190.c:45:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* Generated by Frama-C */
#include "stdlib.h"
long volatile _rand;
long random_long(void)
size_t volatile _rand;
size_t random_size_t(void)
{
return _rand;
}
long packet_get_long_ok(void)
size_t packet_get_size_t_ok(void)
{
long __retres;
size_t __retres;
int tmp_0;
long tmp;
tmp = random_long();
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 0; else tmp_0 = 123456;
__retres = (long)tmp_0;
__retres = (unsigned long)tmp_0;
return __retres;
}
long packet_get_long_problem(void)
size_t packet_get_size_t_problem(void)
{
long tmp_0;
long tmp;
tmp = random_long();
if (tmp) tmp_0 = 9223372036854775807L / (long)2; else tmp_0 = (long)0;
unsigned long tmp_0;
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 18446744073709551615UL / (unsigned long)2 + (unsigned long)1;
else tmp_0 = (unsigned long)0;
return tmp_0;
}
......@@ -37,28 +38,28 @@ int main(void)
{
int __retres;
char **response;
long nresp = packet_get_long_ok();
if (nresp > (long)0) {
response = (char **)malloc((unsigned long)nresp * sizeof(char *));
size_t nresp = packet_get_size_t_ok();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i = (long)0;
size_t i = (unsigned long)0;
while (i < nresp) {
*(response + i) = packet_get_string((char const *)0);
i ++;
i += (size_t)1;
}
}
free((void *)response);
}
nresp = packet_get_long_problem();
if (nresp > (long)0) {
response = (char **)malloc((unsigned long)nresp * sizeof(char *));
nresp = packet_get_size_t_problem();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i_0 = (long)0;
size_t i_0 = (unsigned long)0;
while (i_0 < nresp) {
*(response + i_0) = packet_get_string((char const *)0);
i_0 ++;
i_0 += (size_t)1;
}
}
free((void *)response);
......
[metrics] Defined functions (5)
=====================
main (0 call); packet_get_long_ok (1 call);
packet_get_long_problem (1 call); packet_get_string (2 calls);
random_long (2 calls);
main (0 call); packet_get_size_t_ok (1 call);
packet_get_size_t_problem (1 call); packet_get_string (2 calls);
random_size_t (2 calls);
Specified-only functions (0)
============================
......
......@@ -7,21 +7,21 @@
// Adding option "-warn-unsigned-overflow" ensures Eva reports the
// overflow as soon as it happens.
#include <limits.h>
#include <stdint.h>
#include <stdlib.h>
volatile long _rand;
// returns a random long
long random_long(void) {
volatile size_t _rand;
// returns a random size_t
size_t random_size_t(void) {
return _rand;
}
long packet_get_long_ok() {
return random_long() ? 0 : 123456; // ok size
size_t packet_get_size_t_ok() {
return random_size_t() ? 0 : 123456; // ok size
}
long packet_get_long_problem() {
return random_long() ? LONG_MAX/2 : 0; // too large
size_t packet_get_size_t_problem() {
return random_size_t() ? (SIZE_MAX/2+1) : 0; // too large
}
char *packet_get_string(const char *s) {
......@@ -30,19 +30,19 @@ char *packet_get_string(const char *s) {
int main() {
char **response;
long nresp = packet_get_long_ok();
size_t nresp = packet_get_size_t_ok();
if (nresp > 0) {
response = malloc(nresp*sizeof(char*));
if (!response) exit(1);
for (long i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
for (size_t i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
free(response);
}
nresp = packet_get_long_problem();
nresp = packet_get_size_t_problem();
if (nresp > 0) {
response = malloc(nresp*sizeof(char*));
if (!response) exit(1);
for (long i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
for (size_t i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
free(response);
}
return 0;
......
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