Description
Hello, I'd like to ask you about the solution to the loop problems.
If a project contains about hundreds of loops, do I need an upper bound for each loop? If so, it is difficult to determine the upper bound for each loop. How to solve this problem? I use --unwindset as follows:
cbmc main1.c --unwindset main.2:1,yylex.0:1,yylex.1:1,yylex.2:1,yylex.5:1,yylex.3:1,yylex.6:1,yy_get_previous_state.0:1,yy_get_previous_state.1:1,yylex.8:1,yy_get_next_buffer.0:1,yy_get_next_buffer.1:1,yy_get_next_buffer.2:1,yy_get_next_buffer.3:1,yylex.11:1,yylex.13:1,yylex.12,yyparse.2:1,tri_liste_variable.4:1,tri_liste_variable.5:1,deja_presente.0:1,ajouter_valeur.0:1,initialiser.0:1,tri_liste_variable.0:1,tri_liste_variable.1:1,taille.0:1,tri_liste_variable.2:1,tri_liste_variable.3:1,affecterContraintesDansVariables.0:1,changerTableauxPresence.0:1,enlever_contrainte.0:1,affecterContraintesDansVariables.1:1,affecterContraintesDansVariables.2:1,vider_liste_contrainte:1,videArbre:1,initialiserValeurVariables.0:1,affecterDommaineDansVariables.0:1,concat_variables.0:1,union_domaine.2:1,union_domaine.3:1,creerTableauPresenceVariable.0:1,vider2_pile_domaines:1,liberer_liste.0:1,retournerVariablePortantNom.0:1,retournerVariablePortantNom.1:1,ajouterContraintesDifferent.0:1,yyparse.3:1,yyparse.5:1,yyparse.7:1,premiere_variable.0:1,yylex_destroy.0:1,affecter_valeur.0:1,evalue_contrainte:1,verifier_les_contraintes.0:1,resolutionBacktrackUneSolution.1:1,precedente.1:1,resolutionBacktrackUneSolution.2:1,afficheSolution.0:1,vider_pile_domaines:1,vider_domaine:1
In order to jump out of the loop faster, I used the previous 1, but it didn't work.
If I want to skip a loop, how do I do it? How do use the option --partial-loops?
Thank you!