Feature/new cgc

cgc-challenges/BudgIT/.frama-c/BudgIT.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+CGC_LIB	common.c	139	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ i * (int)(-1)
+CGC_LIB	common.c	139	int2str_dPcdd	signed_overflow	Unknown	i * (int)(-1) ≤ 2147483647
+CGC_LIB	common.c	147	int2str_dPcdd	signed_overflow	Unknown	idx + 1 ≤ 2147483647
+CGC_LIB	common.c	148	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ tmp / 10
+CGC_LIB	common.c	148	int2str_dPcdd	signed_overflow	Unknown	tmp / 10 ≤ 2147483647
+CGC_LIB	common.c	160	int2str_dPcdd	signed_overflow	Unknown	(int)(-1) * (int)(i % 10) ≤ 2147483647
+CGC_LIB	common.c	160	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ (int)(-1) * (int)(i % 10)
+CGC_LIB	common.c	160	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ i % 10
+CGC_LIB	common.c	160	int2str_dPcdd	signed_overflow	Unknown	i % 10 ≤ 2147483647
+CGC_LIB	common.c	161	int2str_dPcdd	signed_overflow	Unknown	(int)'0' + digit ≤ 2147483647
+CGC_LIB	common.c	161	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ (int)'0' + digit
+CGC_LIB	common.c	162	int2str_dPcdd	signed_overflow	Unknown	-2147483648 ≤ i / 10
+CGC_LIB	common.c	162	int2str_dPcdd	signed_overflow	Unknown	i / 10 ≤ 2147483647
+CGC_LIB	libcgc.c	28	cgc_transmit	precondition of write	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
+FRAMAC_SHARE/libc	string.h	115	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
+FRAMAC_SHARE/libc	string.h	138	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
+FRAMAC_SHARE/libc	string.h	352	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	unistd.h	1133	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
+src	map.c	40	cgc_initMap	precondition of memset	Unknown	valid_s: valid_or_empty(s, n)
+src	map.c	49	cgc_initMap	ptr_comparison	Unknown	\pointer_comparable((void *)0, (void *)map_ptr)
+src	map.c	49	cgc_initMap	initialization	Unknown	\initialized(&map_ptr->key[0])
+src	map.c	49	cgc_initMap	mem_access	Unknown	\valid_read(&map_ptr->key[0])
+src	map.c	62	cgc_setMap	ptr_comparison	Unknown	\pointer_comparable((void *)map_ptr, (void *)0)
+src	map.c	62	cgc_setMap	initialization	Unknown	\initialized(&map_ptr->next)
+src	map.c	62	cgc_setMap	mem_access	Unknown	\valid_read(&map_ptr->next)
+src	map.c	63	cgc_setMap	precondition of strcmp	Unknown	valid_string_s2: valid_read_string(s2)
+src	map.c	79	cgc_setMap	mem_access	Unknown	\valid(&map_ptr->next)
+src	map.c	83	cgc_setMap	initialization	Unknown	\initialized(&map_ptr->key[0])
+src	map.c	83	cgc_setMap	mem_access	Unknown	\valid_read(&map_ptr->key[0])
+src	map.c	84	cgc_setMap	precondition of strcpy	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+src	map.c	87	cgc_setMap	mem_access	Unknown	\valid(&map_ptr->value)
+src	map.c	94	cgc_getValue	ptr_comparison	Unknown	\pointer_comparable((void *)map_ptr, (void *)0)
+src	map.c	94	cgc_getValue	initialization	Unknown	\initialized(&map_ptr->next)
+src	map.c	94	cgc_getValue	mem_access	Unknown	\valid_read(&map_ptr->next)
+src	map.c	95	cgc_getValue	ptr_comparison	Unknown	\pointer_comparable((void *)0, (void *)((char *)map_ptr->key))
+src	map.c	95	cgc_getValue	precondition of strcmp	Unknown	valid_string_s2: valid_read_string(s2)
+src	map.c	96	cgc_getValue	initialization	Unknown	\initialized(&map_ptr->value)
+src	map.c	96	cgc_getValue	mem_access	Unknown	\valid_read(&map_ptr->value)
+src	map.c	106	cgc_getSize	ptr_comparison	Unknown	\pointer_comparable((void *)map, (void *)0)
+src	map.c	111	cgc_getSize	initialization	Unknown	\initialized(&last->next)
+src	map.c	111	cgc_getSize	mem_access	Unknown	\valid_read(&last->next)
+src	map.c	111	cgc_getSize	ptr_comparison	Unknown	\pointer_comparable((void *)last->next, (void *)0)
+src	map.c	111	cgc_getSize	signed_overflow	Unknown	size + 1 ≤ 2147483647
+src	map.c	125	cgc_removeMap	ptr_comparison	Unknown	\pointer_comparable((void *)map_ptr, (void *)0)
+src	map.c	125	cgc_removeMap	initialization	Unknown	\initialized(&map_ptr->key[0])
+src	map.c	125	cgc_removeMap	mem_access	Unknown	\valid_read(&map_ptr->key[0])
+src	map.c	125	cgc_removeMap	initialization	Unknown	\initialized(&map_ptr->next)
+src	map.c	125	cgc_removeMap	mem_access	Unknown	\valid_read(&map_ptr->next)
+src	map.c	126	cgc_removeMap	precondition of strcmp	Unknown	valid_string_s2: valid_read_string(s2)
+src	map.c	132	cgc_removeMap	ptr_comparison	Unknown	\pointer_comparable((void *)0, (void *)map_ptr)
+src	map.c	136	cgc_removeMap	initialization	Unknown	\initialized(&map_ptr->next)
+src	map.c	136	cgc_removeMap	mem_access	Unknown	\valid_read(&map_ptr->next)
+src	map.c	138	cgc_removeMap	initialization	Unknown	\initialized(&map_ptr->next)
+src	map.c	138	cgc_removeMap	mem_access	Unknown	\valid(&prev_map_ptr->next)
+src	map.c	138	cgc_removeMap	mem_access	Unknown	\valid_read(&map_ptr->next)
+src	map.c	140	cgc_removeMap	precondition of memset	Unknown	valid_s: valid_or_empty(s, n)
+src	service.c	68	cgc_sendReport	initialization	Unknown	\initialized(&mapPtr->value)
+src	service.c	68	cgc_sendReport	mem_access	Unknown	\valid_read(&mapPtr->value)
+src	service.c	68	cgc_sendReport	signed_overflow	Unknown	-2147483648 ≤ totalBalance + mapPtr->value
+src	service.c	68	cgc_sendReport	signed_overflow	Unknown	totalBalance + mapPtr->value ≤ 2147483647
+src	service.c	79	cgc_sendReport	initialization	Unknown	\initialized(&mapPtr->next)
+src	service.c	79	cgc_sendReport	mem_access	Unknown	\valid_read(&mapPtr->next)
+src	service.c	102	main	initialization	Unknown	\initialized(&instruction)
+src	service.c	105	main	initialization	Unknown	\initialized(&value)
+src	service.c	127	main	initialization	Unknown	\initialized(&value)
+src	service.c	127	main	signed_overflow	Unknown	-2147483648 ≤ budget - value
+src	service.c	127	main	signed_overflow	Unknown	budget - value ≤ 2147483647