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	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	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))
+src	simulation.c	55	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < y_pos * (double)100
+src	simulation.c	55	cgc_simulation_add_particle	float_to_int	Unknown	y_pos * (double)100 < 2147483648
+src	simulation.c	55	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(y_pos, (double)100))
+src	simulation.c	56	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < x_vel * (double)100
+src	simulation.c	56	cgc_simulation_add_particle	float_to_int	Unknown	x_vel * (double)100 < 2147483648
+src	simulation.c	56	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(x_vel, (double)100))
+src	simulation.c	57	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < y_vel * (double)100
+src	simulation.c	57	cgc_simulation_add_particle	float_to_int	Unknown	y_vel * (double)100 < 2147483648
+src	simulation.c	57	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(y_vel, (double)100))
+src	simulation.c	58	cgc_simulation_add_particle	float_to_int	Unknown	-2147483649 < mass * (double)100
+src	simulation.c	58	cgc_simulation_add_particle	float_to_int	Unknown	mass * (double)100 < 2147483648
+src	simulation.c	58	cgc_simulation_add_particle	is_nan_or_infinite	Unknown	\is_finite(\mul_double(mass, (double)100))
+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	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	332	cgc_simulation_run	precondition of fabs	Unknown	finite_arg: \is_finite(x)