search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

More memory issues #180

Closed yanntm closed 4 years ago

yanntm commented 4 years ago

Hi, So, another small bug causing some valgrind complaints.

https://github.com/utwente-fmt/ltsmin/blob/031d920ca8c7703f4cfb94373b82d15960afe0b1/src/mc-lib/lb.c#L115-L122

because of the size_t + cast to int*, the top 4 bytes of "res" are not assigned by random_r.

I get this trace :

==2243== Conditional jump or move depends on uninitialised value(s)
==2243==    at 0x93E3F6: request_random (lb.c:121)
==2243==    by 0x93E95F: lb_internal (lb.c:183)
==2243==    by 0x5ECC95: lb_balance (lb.h:75)
==2243==    by 0x5EDAA8: dfs_fifo_bfs (dfs-fifo.c:229)
==2243==    by 0x5EE272: dfs_fifo_run (dfs-fifo.c:338)
==2243==    by 0x5E88F1: alg_run (algorithm.c:66)
==2243==    by 0x5E4E12: run_alg (run.c:50)
==2243==    by 0x5E0AAF: main (pins2lts-mc.c:209)
==2243==  Uninitialised value was created by a stack allocation
==2243==    at 0x93E363: request_random (lb.c:114)
==2243== 
==2243== Use of uninitialised value of size 8
==2243==    at 0x93E423: request_random (lb.c:122)
==2243==    by 0x93E95F: lb_internal (lb.c:183)
==2243==    by 0x5ECC95: lb_balance (lb.h:75)
==2243==    by 0x5EDAA8: dfs_fifo_bfs (dfs-fifo.c:229)
==2243==    by 0x5EE272: dfs_fifo_run (dfs-fifo.c:338)
==2243==    by 0x5E88F1: alg_run (algorithm.c:66)
==2243==    by 0x5E4E12: run_alg (run.c:50)
==2243==    by 0x5E0AAF: main (pins2lts-mc.c:209)
==2243==  Uninitialised value was created by a stack allocation
==2243==    at 0x93E363: request_random (lb.c:114)

I think using size_t res=0 at line 115 should solve the issue, the type is still too large for the use that is made of it (random is not producing a random size_t) but it suppresses the error.

yann

yanntm commented 4 years ago

this is closed by the accepted PR https://github.com/utwente-fmt/ltsmin/pull/182