Project

General

Profile

« Previous | Next » 

Revision 033be72c

Added by Pierre-Loïc Garoche over 4 years ago

Seal targets

View differences:

regression_tests/modules/Lustre_compile.cmake
85 85
  NO_DEFAULT_PATH
86 86
  DOC "Path to the Lustre compiler command 'lustret'")
87 87

  
88
find_program(LUSTRE_V
89
  NAMES lustrev
90
  HINTS ${LUSTRE_PATH_HINT}
91
  PATH_SUFFIXES bin
92
  DOC "Path to the Lustre compiler command 'lustrev'")
93

  
94
find_program(LUSTRE_V
95
  NAMES lustrev
96
  PATHS ${LUSTRE_PATH_HINT}
97
  PATH_SUFFIXES bin
98
  NO_DEFAULT_PATH
99
  DOC "Path to the Lustre compiler command 'lustrev'")
100

  
88 101
	
89 102
# Macros used to compile a lustre library
90 103
include(CMakeParseArguments)
regression_tests/modules/strategies.cmake
655 655
    DEPENDS ${GEN_TESTS_PREFIX}_ADA_BIN_${L}_${GEN_NODE}_${LUS_OPTS_CUT}_${GEN_CALL_ID} )
656 656

  
657 657
endfunction()
658

  
659

  
660
#****************************** LustreV strategies: generating the SEAL encoding and check it with kind2 
661

  
662

  
663
function(LustreV_SEAL_kind2)
664
  set(options "")
665
  set(oneValueArgs  NODE LUS_FILE CALL_ID TESTS_PREFIX SRC_DIR DST_DIR)
666
  set(multiValueArgs  OPTS )
667
  cmake_parse_arguments(GEN "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
668

  
669
  find_program(KIND2
670
  NAMES kind2
671
   HINTS ${LUSTRE_PATH_HINT}
672
   DOC "Path to the Kind2 model-checker")
673

  
674
  get_lustre_name_ext(${GEN_LUS_FILE} L E)
675
    Lustre_Compile(LUS_FILE ${GEN_LUS_FILE}
676
    NODE ${GEN_NODE}
677
    OPTS ${GEN_OPTS}
678
    DIR "${GEN_DST_DIR}/${L}/node_${GEN_NODE}_SEAL"
679
#    DST_DIR ${GEN_DST_DIR}
680
    )
681

  
682
  file(MAKE_DIRECTORY "${GEN_DST_DIR}/${L}/node_${GEN_NODE}_SEAL")
683
  # First test: create the seal export files. Use kind2 syntax for the moment
684
  add_test(NAME ${GEN_TESTS_PREFIX}_LUSTREV_SEAL_GEN_${L}_${GEN_NODE}_${LUS_OPTS_CUT}_${GEN_CALL_ID}  
685
    COMMAND  ${LUSTRE_V} -seal -seal-export lustre -kind2 ${LUSTREC_ARGS_${L}_${GEN_NODE}_${LUS_OPTS_CUT}}
686
    WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${GEN_NODE}_${LUS_OPTS_CUT}}
687
    )
688
  
689
  set(SEAL_GEN_SRC "${GEN_DST_DIR}/${L}/node_${GEN_NODE}_SEAL/${L}_seal_verif.lus")
690
 
691
  
692
  add_test(NAME ${GEN_TESTS_PREFIX}_LUSTREV_SEAL_KIND2_${L}_${GEN_NODE}_${LUS_OPTS_CUT}_${GEN_CALL_ID}
693
    COMMAND  sh -c "${KIND2} --lus_main check_eq_${GEN_NODE}_seal_${GEN_NODE} -q ${SEAL_GEN_SRC} |grep guarantee | grep -c \"valid\""
694
    WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}__${GEN_NODE}_${LUS_OPTS_CUT}}
695
    )
696
  
697
  SET_TESTS_PROPERTIES ( ${GEN_TESTS_PREFIX}_LUSTREV_SEAL_KIND2_${L}_${GEN_NODE}_${LUS_OPTS_CUT}_${GEN_CALL_ID}
698
    PROPERTIES 
699
    DEPENDS ${GEN_TESTS_PREFIX}_LUSTREV_SEAL_GEN_${L}_${GEN_NODE}_${LUS_OPTS_CUT}_${GEN_CALL_ID})
700
  
701
endfunction()

Also available in: Unified diff