MATLAB: Do I receive a message ‘No space left on device’ when using PolySpace for C/C++ on server side

diskfullmemoryofoutpolyspacePolyspace Code ProverPolyspace Code Prover Serverunix

When I launch a verification on PolySpace server, I receive an error:
 
*** Software Safety Analysis Level N …
System error No space left on device (nospc: No space left on device)"

Best Answer

The error is seen because one of the disk locations is probably full (as mentioned in the error message). On the PolySpace server, there are two locations where PolySpace can take up disk space:
  • in /var/PolySpace or on in PolySpace_RLDatas sub-folder (location is given in polyspace.conf file)
  • in /tmp or in location given by %TEMP% environment variable.
As soon as this message appears, check the two locations.
On a UNIX system, if it concerns /tmp location, it is possible to redirect the TMP used by PolySpace onto /var for instance (if for instance there is enough space in /var). In bash shell, it gives:
 
mkdir /var/polyspace_tmp
RTE_TMP_DIR=/var/polyspace_tmp
export RTE_TMP_DIR
But as verification is launched through Queue Manager, this environment variable must be given to the Queue Manager login account. To do that, login on server machine as login account and execute the following commands (last command starts polyspaced outside service):
 
/etc/init.d/polyspaced stop
RTE_TMP_DIR=/var/polyspace_tmp
export RTE_TMP_DIR
$POLYSPACE_COMMON/RemoteLauncher/bin/polyspaced
Then you can relaunch the verification. If it fixes the trouble and as the Queue Manager is launched as a service, please put the environment variable in the startup script:
 
kill process associated with polyspaced (you launched polyspaced outside service management above)
edit /etc/init.d/polyspaced and add 'export RTE_TMP_DIR=/var/polyspace_tmp' around line 15 and save file
/etc/init.d/polyspaced start
Notes:
1. Previous hints have to be slightly adapted for a Windows OS.
2. Since R2012b, following batch option forces to locate temporary files in a results sub-folder:
-tmp-dir-in-results-dir