Feature/new cgc

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

 directory	file	line	function	property kind	status	property
 CGC_LIB	libcgc.c	172	cgc_allocate	precondition	Unknown	valid_addr: \valid((char *)*addr)
+FRAMAC_SHARE/libc	math.h	449	fabs	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	493	sqrt	precondition	Unknown	finite_arg: \is_finite(x)
 src	render.c	47	cgc_init_render_grid	precondition of cgc_allocate	Unknown	valid_addr: \valid((char *)*addr)
-src	render.c	72	cgc_init_render_grid	mem_access	Unknown	\valid(&(g_renderGrid + grid_position)->bounds_x)
 src	render.c	94	cgc_add_render_grid	float_to_int	Unknown	-1 < pItem->x_pos - (double)100
 src	render.c	94	cgc_add_render_grid	float_to_int	Unknown	pItem->x_pos - (double)100 < 4294967296
+src	render.c	94	cgc_add_render_grid	is_nan_or_infinite	Unknown	\is_finite(\sub_double(pItem->x_pos, (double)100))
 src	render.c	95	cgc_add_render_grid	float_to_int	Unknown	-1 < pItem->y_pos - (double)100
 src	render.c	95	cgc_add_render_grid	float_to_int	Unknown	pItem->y_pos - (double)100 < 4294967296
+src	render.c	95	cgc_add_render_grid	is_nan_or_infinite	Unknown	\is_finite(\sub_double(pItem->y_pos, (double)100))
 src	render.c	107	cgc_add_render_grid	initialization	Unknown	\initialized(&(g_renderGrid + (unsigned int)((unsigned int)(render_grid_x * 20) + render_grid_y))->particles_in_grid)
 src	render.c	124	cgc_display_render_grid	initialization	Unknown	\initialized(&(g_renderGrid + grid_position)->particles_in_grid)
 src	service.c	66	cgc_readLine	initialization	Unknown	\initialized((char *)temp_buffer)
-src	service.c	88	cgc_parse_float_pair	initialization	Unknown	\initialized(buf + pos)
-src	service.c	106	cgc_parse_float_pair	initialization	Unknown	\initialized(buf + pos)
-src	service.c	193	main	is_nan_or_infinite	Unknown	\is_finite(mass)
-src	service.c	206	main	is_nan_or_infinite	Unknown	\is_finite(radius)
-src	service.c	213	main	initialization	Unknown	\initialized(&pos_x)
-src	service.c	213	main	initialization	Unknown	\initialized(&pos_y)
-src	service.c	213	main	initialization	Unknown	\initialized(&vel_x)
-src	service.c	213	main	initialization	Unknown	\initialized(&vel_y)
-src	service.c	213	main	is_nan_or_infinite	Unknown	\is_finite(pos_x)
-src	service.c	213	main	is_nan_or_infinite	Unknown	\is_finite(pos_y)
-src	service.c	213	main	is_nan_or_infinite	Unknown	\is_finite(vel_x)
-src	service.c	213	main	is_nan_or_infinite	Unknown	\is_finite(vel_y)
+src	service.c	216	main	initialization	Unknown	\initialized(&pos_x)
+src	service.c	216	main	initialization	Unknown	\initialized(&pos_y)
+src	service.c	216	main	initialization	Unknown	\initialized(&vel_x)
+src	service.c	216	main	initialization	Unknown	\initialized(&vel_y)
 src	simulation.c	54	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < x_pos * (double)100
 src	simulation.c	54	cgc_simulation_add_particle	float_to_int	Unknown	x_pos * (double)100 < 2147483648
 src	simulation.c	54	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(x_pos, (double)100))
@@ -39,61 +34,13 @@ src	simulation.c	58	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_f
 src	simulation.c	59	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < radius * (double)100
 src	simulation.c	59	cgc_simulation_add_particle	float_to_int	Unknown	radius * (double)100 < 2147483648
 src	simulation.c	59	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(radius, (double)100))
-src	simulation.c	123	cgc_is_colliding	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->x_pos, p2->x_pos))
-src	simulation.c	124	cgc_is_colliding	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->y_pos, p2->y_pos))
-src	simulation.c	128	cgc_is_colliding	is_nan_or_infinite	Unknown	\is_finite(\add_double(\mul_double(x_delta, x_delta), \mul_double(y_delta, y_delta)))
-src	simulation.c	128	cgc_is_colliding	is_nan_or_infinite	Unknown	\is_finite(\mul_double(x_delta, x_delta))
-src	simulation.c	128	cgc_is_colliding	is_nan_or_infinite	Unknown	\is_finite(\mul_double(y_delta, y_delta))
-src	simulation.c	142	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->x_pos, p2->x_pos))
-src	simulation.c	143	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->y_pos, p2->y_pos))
-src	simulation.c	145	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(\mul_double(delta_x, delta_x), \mul_double(delta_y, delta_y)))
-src	simulation.c	145	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_x, delta_x))
-src	simulation.c	145	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_y, delta_y))
-src	simulation.c	151	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\div_double(radius_total, delta_length))
-src	simulation.c	154	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_x, radius_scale))
-src	simulation.c	155	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_y, radius_scale))
-src	simulation.c	162	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_x))
-src	simulation.c	163	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_y))
-src	simulation.c	165	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\div_double(mass2, total_mass))
-src	simulation.c	166	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\div_double(mass1, total_mass))
-src	simulation.c	168	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(temp_mtdx_double, mass1_ratio))
-src	simulation.c	169	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(temp_mtdy_double, mass1_ratio))
-src	simulation.c	171	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->x_pos, x_position_change1))
-src	simulation.c	172	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->y_pos, y_position_change1))
-src	simulation.c	174	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(temp_mtdx_double, mass2_ratio))
-src	simulation.c	175	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(temp_mtdy_double, mass2_ratio))
-src	simulation.c	177	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p2->x_pos, x_position_change2))
-src	simulation.c	178	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p2->y_pos, y_position_change2))
-src	simulation.c	188	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->x_vel, p2->x_vel))
-src	simulation.c	189	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p1->y_vel, p2->y_vel))
-src	simulation.c	191	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(\mul_double(mtd_x, mtd_x), \mul_double(mtd_y, mtd_y)))
-src	simulation.c	191	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(mtd_x, mtd_x))
-src	simulation.c	191	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(mtd_y, mtd_y))
-src	simulation.c	198	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\div_double(mtd_x, mtd_length))
-src	simulation.c	199	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\div_double(mtd_y, mtd_length))
-src	simulation.c	202	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(\mul_double(delta_velocity_x, normal_mtd_x), \mul_double(delta_velocity_y, normal_mtd_y)))
-src	simulation.c	202	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_velocity_x, normal_mtd_x))
-src	simulation.c	202	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(delta_velocity_y, normal_mtd_y))
-src	simulation.c	208	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)((int)(-2)), velocity_normal))
-src	simulation.c	210	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(normal_mtd_x, impulse))
-src	simulation.c	211	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(normal_mtd_y, impulse))
-src	simulation.c	214	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->x_vel, \mul_double(impulse_x, mass1_ratio)))
-src	simulation.c	214	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(impulse_x, mass1_ratio))
-src	simulation.c	215	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->y_vel, \mul_double(impulse_y, mass1_ratio)))
-src	simulation.c	215	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(impulse_y, mass1_ratio))
-src	simulation.c	217	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p2->x_vel, \mul_double(impulse_x, mass2_ratio)))
-src	simulation.c	217	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(impulse_x, mass2_ratio))
-src	simulation.c	218	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\sub_double(p2->y_vel, \mul_double(impulse_y, mass2_ratio)))
-src	simulation.c	218	cgc_do_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double(impulse_y, mass2_ratio))
-src	simulation.c	243	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_x))
-src	simulation.c	258	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->x_pos, \mul_double((double)2, mtd_x_0)))
-src	simulation.c	258	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_x_0))
-src	simulation.c	273	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_y))
-src	simulation.c	287	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\add_double(p1->y_pos, \mul_double((double)2, mtd_y_0)))
-src	simulation.c	287	cgc_do_wall_collision	is_nan_or_infinite	Unknown	\is_finite(\mul_double((double)2, mtd_y_0))
+src	simulation.c	147	cgc_do_collision	precondition of sqrt	Unknown	finite_arg: \is_finite(x)
+src	simulation.c	196	cgc_do_collision	precondition of sqrt	Unknown	finite_arg: \is_finite(x)
+src	simulation.c	325	cgc_simulation_run	precondition of fabs	Unknown	finite_arg: \is_finite(x)
 src	simulation.c	326	cgc_simulation_run	float_to_int	Unknown	tmp / g_particles[i].radius < 4294967296
 src	simulation.c	326	cgc_simulation_run	is_nan_or_infinite	Unknown	\is_finite(\div_double(tmp, g_particles[i].radius))
+src	simulation.c	326	cgc_simulation_run	precondition of fabs	Unknown	finite_arg: \is_finite(x)
+src	simulation.c	331	cgc_simulation_run	precondition of fabs	Unknown	finite_arg: \is_finite(x)
 src	simulation.c	332	cgc_simulation_run	float_to_int	Unknown	tmp_1 / g_particles[i].radius < 4294967296
 src	simulation.c	332	cgc_simulation_run	is_nan_or_infinite	Unknown	\is_finite(\div_double(tmp_1, g_particles[i].radius))
-src	simulation.c	359	cgc_simulation_run	is_nan_or_infinite	Unknown	\is_finite(\add_double(g_particles[i].x_pos, temp_x_vel))
-src	simulation.c	360	cgc_simulation_run	is_nan_or_infinite	Unknown	\is_finite(\add_double(g_particles[i].y_pos, temp_y_vel))
+src	simulation.c	332	cgc_simulation_run	precondition of fabs	Unknown	finite_arg: \is_finite(x)