Re: [MRMC] [patch] Bug in timings on x86

Hi Bram,

Thanks for your report. I'll have the patch archived for the next release.

Note that the ticket link only works for frequent committers.

Viet Yen

On 19.12.11, Bram Geron bgeron@gmail.com wrote:

Hi,

On my 32-bit machine MRMC gives incorrect timings. This is due to
the fact that the clock type is converted to an unsigned long,
which is 32-bit on 32-bit systems. A patch follows, which also fixes
a typo.



By the way, the new ticket link at mrmc-tool.org/trac/wiki/Contact(http://www.mrmc-tool.org/trac/wiki/Contact)
doesn't work, because it wants me to log in and I can't seem to make
an account.



Cheers,



Bram Geron

CS student at Eindhoven University of Technology





--- a/src/io/parser/parser_to_core.c    Mon Dec 19 17:13:47 2011
  +0100

  +++ b/src/io/parser/parser_to_core.c    Mon Dec 19 17:28:30 2011
  +0100

  @@ -103,7 +103,7 @@

           }

   

           timer_started = FALSE;

  -        return ((unsigned long) (stop_time - start_time) * 1000

  +        return ((clock_t) (stop_time - start_time) * 1000

                           + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC;

   }

   

  @@ -567,7 +567,7 @@

          /* Clean the old results */

          clearOldModelCheckingResults();

   

  -       /* Star the timer */

  +       /* Start the timer */

          startTimer();

   

          /* In case of simulation engine on we have to traverse the
  tree */

---

MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users