Makefile configuration

  • To make T-Check work, add 
              	PFLAGS += -fnesc-mc-state
    into the application Makefile. Note that this flag is required

  • If users want to specify high-level safety or liveness property, add 
              CFLAGS += -DSAFETY 
          CFLAGS += -DLIVENESS 
          CFLAGS += -D(SYMBOL)
    into the application Makefile. Note that for SAFETY and LIVENESS flags, whether either one or both are added depends on which kinds of properties to be checked. (SYMBOL) denotes the [Application symbol] used as the argument of "preprocessing" perl script.

  • If users want to activate the hardware part, add 
              CFLAGS += -DADCON  (ADC is on)      
          CFLAGS += -DUARTON  (UART is on)
          CFLAGS += -DSIM_CC2420 (Byte-level transmission is activated, 
          but do not recommend to use this option due to its impediment for high-level property checking)
    into the application Makefile.

  • If users want to test applications, which do not contain any communication components, such as NULL, Blink..., add 
             CFLAGS += -DSIM_ASSIST_COMM
    into the application Makefile.

  • If users want to test applications, which do not contain any timer components, such as TestADC..., add 
             CFLAGS += -DSIM_ASSIST_TIMER
    into the application Makefile.

  • If you want to test TestFtsp application, please add 
             CFLAGS += -DTIMESYNC
    into the application Makefile. Note that this is a special case.