diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh index 003db5f0f80ba222d5681d98f80449198de48830..836e008346c3c00263797b92e82ef935672d2685 100755 --- a/bin/build-src-distrib.sh +++ b/bin/build-src-distrib.sh @@ -23,9 +23,9 @@ if ! command -v git-lfs >/dev/null 2>/dev/null; then exit 99 fi -# rgrep needs to be installed -if ! command -v rgrep --version >/dev/null 2>/dev/null; then - echo "rgrep is required" +# grep needs to be installed +if ! command -v grep --version >/dev/null 2>/dev/null; then + echo "grep is required" exit 99 fi @@ -100,7 +100,7 @@ function look_for_uncommited_changes { } function look_for_frama_c_dev { - rgrep -i "frama-c+dev" src &> /dev/null + grep -Iir "frama-c+dev" src &> /dev/null if [ "$?" == "0" ]; then echo "### WARNING: Remaining frama-c+dev occurrences in 'src'" proceed_anyway "Update API, then run the script again" @@ -251,12 +251,15 @@ function fill_wiki { function add_install_page { INSTALL_WEBPAGE=html/installations/$FRAMAC_VERSION_CODENAME_LOWER.md INSTALL_WEBPAGE_PATH=$WEBSITE_DIR/$INSTALL_WEBPAGE + EXT="$FRAMAC_VERSION_CODENAME (released on $(date +%Y-%m-%d))" echo "---" > $INSTALL_WEBPAGE_PATH - echo "layout: doc_page" >> $INSTALL_WEBPAGE_PATH + echo "layout: installation_page" >> $INSTALL_WEBPAGE_PATH + echo "version: $FRAMAC_VERSION_CODENAME_LOWER" >> $INSTALL_WEBPAGE_PATH echo "title: Installation instructions for $FRAMAC_VERSION_CODENAME" >> $INSTALL_WEBPAGE_PATH echo "---" >> $INSTALL_WEBPAGE_PATH echo >> $INSTALL_WEBPAGE_PATH - cat ./INSTALL.md >> $INSTALL_WEBPAGE_PATH + cat ./INSTALL.md |\ + sed -e "s/^\(# Installing Frama-C\)$/\1 $EXT/" >> $INSTALL_WEBPAGE_PATH run "git -C $WEBSITE_DIR add $INSTALL_WEBPAGE" } @@ -470,6 +473,7 @@ function create_website_branch { echo "### Warning: branch $BRANCH_NAME already exists in $WEBSITE_DIR" echo "The script will ERASE this branch" proceed_anyway "Rename or erase the branch, then run the script again." + run "git -C $WEBSITE_DIR checkout master" run "git -C $WEBSITE_DIR branch -D $BRANCH_NAME" fi @@ -487,7 +491,7 @@ function create_website_branch { run "git -C $WEBSITE_DIR checkout master" exit 1 esac - run "git -C $WEBSITE_DIR commit -m \"Prepare pages for the release of Frama-C $FRAMAC_VERSION\"" + run "git -C $WEBSITE_DIR commit -m \"$FRAMAC_VERSION_AND_CODENAME release\"" } function commit_wiki { @@ -502,7 +506,7 @@ function commit_wiki { echo "Abort wiki update." exit 1 esac - run "git -C $WIKI_DIR commit -m \"Prepare pages for the release of Frama-C $FRAMAC_VERSION\"" + run "git -C $WIKI_DIR commit -m \"$FRAMAC_VERSION_AND_CODENAME release\"" } @@ -520,10 +524,10 @@ function last_step_validation { This step will: - ask for a validation of the changes to website - - create a NEW branch on for the website + - create a NEW local branch for the website - ask for a validation of the changes to wiki - - commit changes to the wiki MASTER branch + - commit changes to the wiki MASTER local branch If you want to perform some additional checks it is probably time to stop. @@ -796,7 +800,6 @@ case "${STEP}" in echo "Bad entry: ${STEP}" echo "Exiting without doing anything."; exit 31 - ;; esac exit 0 diff --git a/doc/release/build.tex b/doc/release/build.tex index e3c9386b25c4516fd10187fffbc1b047d526c18a..4eec599e4e42c8d1ccad4ed6bfb54aaa28499902 100644 --- a/doc/release/build.tex +++ b/doc/release/build.tex @@ -329,7 +329,7 @@ Please check that the distribution (sources and API) is OK: \item \verb+./configure --prefix="$PWD/build"+ \item \verb+make+; \item \verb+make install+; - \item \verb+rm -f ~/.why3.conf; why3 config --detect+; + \item \verb+rm -f ~/.why3.conf; why3 config detect+; \item \verb+build/bin/frama-c tests/idct/*.c -eva -wp -wp-rte+ \item If you have a GUI, replace \verb+frama-c+ above with \verb+frama-c-gui+ and click around, see if things work (e.g. no segmentation faults). diff --git a/doc/release/website.tex b/doc/release/website.tex index 6e6b79dc3aec6550a8aebbb00c3a994bc2333011..07703879f00911bc5c938ebd7abd477e3d53eab0 100644 --- a/doc/release/website.tex +++ b/doc/release/website.tex @@ -37,11 +37,23 @@ Check the following pages: \item check ACSL version. \end{itemize} \item \texttt{/html/changelog.html\#Version-NN.N} - \item \texttt{/html/installations/titanium.html} \item \texttt{/html/acsl.html}: check ACSL versions list \item \texttt{rss.xml}: check last event \end{itemize} +For a beta version, the installation pages for: +\begin{itemize} +\item \texttt{/html/installations/beta\_version\_name.html} should indicate the beta status +\item \texttt{/html/installations/current\_version\_name.html} should not indicate anything +\item \texttt{/html/installations/previous\_version\_name.html} should indicate older version +\end{itemize} + +For a final version, the installation pages for: +\begin{itemize} +\item \texttt{/html/installations/version\_name.html} should not indicate anything +\item \texttt{/html/installations/previous\_version\_name.html} should indicate older version +\end{itemize} + On GitLab, the following files must appear as \textbf{new} in \texttt{download}. Note that for beta versions, if you have not included all manuals, not all of them will appear: diff --git a/doc/value/examples/parametrizing/context-depth.c b/doc/value/examples/parametrizing/context-depth.c index 4ced05618bc4c547a640b48684847a1fd76613f6..fa3271d3d7a4f8ff4596b485c14e19525a561dbf 100644 --- a/doc/value/examples/parametrizing/context-depth.c +++ b/doc/value/examples/parametrizing/context-depth.c @@ -1,4 +1,4 @@ -struct S { int v; struct S *next; }; +struct S { long v; struct S *next; }; struct S s; diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli index b36711a37e01b07ee90e856f2847359654c8d673..adbc32c1652bba6b9432d70578c2981f6640c837 100644 --- a/src/plugins/rte/flags.mli +++ b/src/plugins/rte/flags.mli @@ -67,10 +67,10 @@ val default : ?bool_value:bool -> unit -> t -(** All flags set to [true], [@all] for [initialized] *) +(** All flags set to [true], "@all" for initialized *) val all : unit -> t -(** All flags set to [false], [empty] for [initialized] *) +(** All flags set to [false], empty for initialized *) val none : t (* -------------------------------------------------------------------------- *)